The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Introducing any new technology involves organisational, skill, method and tool changes, which require a commitment from the industry concerned. The introduction of formal methods into system and software design is no exception. Before the widespread use of formal methods can be achieved, it will be necessary for the IT industry to convince itself that the methods are genuinely usable in an industrial...
Since 1980, three different formal descriptions of the Ada programming language have been developed, based on the principles of the Vienna Development Method (VDM). This paper characterizes each of the three descriptions and explains some of the differences.
Since 1982 NORSK DATA and the University of Kiel, Germany, have been cooperating in the area of compiler development. During this time a multilanguage multi-target compiler system has been developed using the Vienna Development Method (VDM) and its specification language, META IV A common intermediate language has been derived from the denotational semantic specifications of the source languages and...
In this paper the Vienna Development Method (VDM) is related to the various phases of activities throughout the process of software development. Several shortcomings of VDM are discussed and the combination of Object-Oriented Design (OOD) techniques, enriched by guidelines from the Jackson System Design method (JSD), with VDM is examined. The use of VDM to derive Ada package software is discussed.
In VDM development of software proceeds from specification, via stages of design, to coding. A classical way of illustrating this is by the "waterfall- diagram" of fig.3. As a planning aid, drawing such simple sequences of boxes as shown in fig. 3. really is of no help. In this paper we shall carefully develop an example, so-called software development graph. Thus from a graph like...
Improved software development techniques can be introduced only if their advantage can be demonstrated even without major investments. We suggested to start by changeing low level specifications while still keeping them close to the implementation language and to a smoothly extended environment. So use and adaption to a given context of "the Method" have been of interest here. Our...
This paper discusses the experiences and issues of building two different levels of system to support the use of VDM. The MULE system is an example of an environment giving support in the syntactic generation of formal objects, such as specifications. The IPSE 2.5 system is an attempt to produce an industrial scale system to support the use of formal methods over the whole of a software...
A method using VDM and its meta language META IV for systematic semi-automated compiler development is outlined. Then the construction of a META IV compiler sophisticated enough to extend that method to a fully automated one is described. After the introduction of a compilable subset of META IV the implementation of fixpoints and implicitly defined sets, maps and tuples will be discussed. Another...
Although VDM — the Vienna Development Method — has probably been the most widespread and popular so-called formal method for software development in use so far, it is clear that VDM suffers from a number of deficiencies. In this paper, the transition from VDM to a new, “second generation” formal method — RAISE — is discussed. Problems with VDM are discussed, and their solutions within RAISE are outlined...
This paper is devoted to the methodology of using denotational techniques in software design. Since denotations describe the mechanisms of a system and syntax is only a user-visible representation of these mechanisms, we suggest that denotations be developed in the first place and that syntax be derived from them later. That viewpoint is opposite to the traditional (descriptive) style where denotational...
A model of types for use in VDM specifications is presented. Standard VDM types consisting of finitary values are given set-theoretic denotations, restricting the use of Scott domain theory to the provision of types for the continuous functions and Bekic mappings. An objective of this work was to give a simple account of recursively defined data types not involving the full apparatus surrounding the...
“The Vienna Development Method” (VDM) uses specifications built in terms of models and operations specified by pre-/post-conditions. Steps of design by data reification or operation decomposition give rise to proof obligations. This paper provides examples of both sorts of design step but its main intention is to show that the proof obligations for operation decomposition are consistent with a semantics...
This paper presents a formal description of a non-conventional machine architecture (The Manchester DataFlow Machine) in the denotational style, using an extension of the traditional VDM methods. The semantics is defined in terms of two fixed-point expressions over a relational domain. Some general and specific properties of such a semantics are presented.
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.